"""These classes provide support to represent and evaluate
propositional logic.

Danny Yoo (dyoo@hkn.eecs.berkeley.edu)
"""
from __future__ import nested_scopes


def nodeEval(node, env=None):
    """A functional wrapper that simply calls a node's eval()
    function."""
    return node.eval(env)


class Node:
    def __init__(self, type, attr, left=None, right=None, children=()):
        self.type = type
        self.attr = attr
        self.children = list(children)
        if left: self.children.append(left)
        if right: self.children.append(right)


    def __getitem__(self, i):
        return self.children[i]

 
    def isLeaf(self):
        return len(self.children) == 0
 

    def __str__(self):
        if self.isLeaf(): return "%s" % self.attr
        child_list = map(str, self.children)
        if self.attr == None:
            return "%s[%s]" % (self.type, ', '.join(child_list))
        else:
            return "%s[%s]" % (self.attr, ', '.join(child_list))

    ## Something of an abuse of __repr__ --- I may want to change this to
    ## follow Pythonic repr() conventions.
    __repr__ = __str__

    def eval(self, env):
        """Evaluate a node, given a particular env binding that binds
        identifiers to values, and return that value."""
        print "I haven't been defined yet.  Fixme!"



class TrueNode(Node):
    """Represents "TRUE" in our propositional system."""
    def __init__(self):
        Node.__init__(self, type='constant', attr='tt')

    def eval(self, env):
        return self

    def __eq__(self, other):
        return isinstance(other, TrueNode)
    

class FalseNode(Node):
    """Represents "FALSE" in our propositional system."""
    def __init__(self):
        Node.__init__(self, type='constant', attr='ff')

    def eval(self, env):
        return self

    def __eq__(self, other):
        return isinstance(other, FalseNode)

"""Definitions of TRUE_VALUE and FALSE_VALUE use nodes, so that
eval() is mathematically "closed" as a node operation."""
TRUE_VALUE = TrueNode()
FALSE_VALUE = FalseNode()



class ImplicationNode(Node):
    def __init__(self, left, right):
        Node.__init__(self, type='implication', attr=None,
                      left=left, right=right)

    def eval(self, env):
        if self[0].eval(env) == FALSE_VALUE:
            return TRUE_VALUE
        elif self[1].eval(env) == TRUE_VALUE:
            return TRUE_VALUE
        else:
            return FALSE_VALUE


class EqualityNode(Node):
    def __init__(self, left, right):
        Node.__init__(self, type='equality', attr=None,
                      left=left, right=right)

    def eval(self, env):
        return primitiveEquals(self[0].eval(env), self[1].eval(env))

    ## Hmmm... this may need to be fixed.  In retrospect, I don't think
    ## this is a robust definition.

    
class EuNode(Node):
    def __init__(self, *children):
        Node.__init__(self, type='eU', attr=None,
                      children=children)

    def eval(self, env):
        values = map(lambda c: c.eval(env), self.children)
        return primitiveAnd(*values)

class AuNode(Node):
    def __init__(self, *children):
        Node.__init__(self, type='aU', attr=None,
                      children=children)

    def eval(self, env):
        values = map(lambda c: c.eval(env), self.children)
        return primitiveAnd(*values)

class AndNode(Node):
    def __init__(self, *children):
        Node.__init__(self, type='and', attr=None,
                      children=children)

    def eval(self, env):
        values = map(lambda c: c.eval(env), self.children)
        return primitiveAnd(*values)
        

class OrNode(Node):
    def __init__(self, *children):
        Node.__init__(self, type='or', attr=None,
                      children=children)

    def eval(self, env):
        values = map(lambda c: c.eval(env), self.children)
        return primitiveOr(*values)


class NotNode(Node):
    def __init__(self, node):
        Node.__init__(self, type='not', attr=None,
                      children=[node])

    def eval(self, env):
        value = self[0].eval(env)
        return primitiveNot(value)


class AatNode(Node):
    def __init__(self, node):
        Node.__init__(self, type='aAT', attr=None,
                      children=[node])

    def eval(self, env):
        value = self[0].eval(env)
        return primitiveNot(value)
    
class EatNode(Node):
    def __init__(self, node):
        Node.__init__(self, type='eAT', attr=None,
                      children=[node])

    def eval(self, env):
        value = self[0].eval(env)
        return primitiveNot(value)
    

class IdentifierNode(Node):
    def __init__(self, identifier):
        Node.__init__(self, type='identifier', attr=identifier)

    def eval(self, env):
        if env.has_key(self.attr): return env[self.attr]
        return self
        ## fixme!  I want to implement nestable environments, and make
        ## this more robust.
    

def primitiveAnd(*values):
    for v in values:
        if v == FALSE_VALUE:
            return FALSE_VALUE
    return TRUE_VALUE


def primitiveOr(*values):
    for v in values:
        if v == TRUE_VALUE:
            return TRUE_VALUE
    return FALSE_VALUE


def primitiveNot(value):
    if value == TRUE_VALUE:
        return FALSE_VALUE
    return TRUE_VALUE


def primitiveEquals(lhs, rhs):
    if lhs == rhs: return TRUE_VALUE
    return FALSE_VALUE


def primitiveTrue(x):
    return x == TRUE_VALUE


def primitiveFalse(x):
    return x == FALSE_VALUE
